i:, j:{i+1...}, E:({i..j}{u}).
E(i)  (k:{(i+1)..j}. E(k - 1)  E(k))  {k:{i..j}. E(k)} 

latex

Up	int 2, int 2
Definitions	False, A, P & Q, i  j < k, A  B, t  T, {T}, x(s), P  Q, , {i..j}, x:A. B(x), x. t(x), {i...}, WellFnd{i}(A;x,y.R(x;y)), P  Q, Dec(P)
Lemmas	int upper wf, le wf, int seg wf, int seg well founded up, decidable int equal